-- -*-Haskell-*-

{-
 * Copyright (c) 2007-2011 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}

-- Usage:
--
--  Set up the environment
--     setenv LD_LIBRARY_PATH /opt/exp/gnu/lib:$LD_LIBRARY_PATH
--     setenv PATH /home/ggreif/%NoBackup%/Omega1.4:$PATH
--
--  Start the omega interpreter by typing
--     omega AdministrativeNormalForm.omg
--  and run your commands on the prompt
--

import "LangPrelude.prg" 
  (head,tail,lookup,member,fst,snd,map,Monad,maybeM,id,ioM,Row,HasType,RCons,RNil,Eq,Equal)


-- This document is a tentative to formalize the system
-- "The Essence of Compiling Call-by-Need"
-- by Amr Sabry (1999).

-- Figure 1 introduces the source language (CBV variant)

-- Terms e ::= x | \x.e | ee | let x = e in e | letrec xi = vi in e
-- Values v ::= \x.e
-- Types tau ::= b | tau -> tau

kind SrcCat = T | V

data Src :: SrcCat ~> * where
  Var :: Label l -> Src T
  Lam :: Label l -> Src a -> Src V
  App :: Src a -> Src b -> Src T
  Let :: Label l -> Src a -> Src b -> Src T
  LetRec :: Label l -> Src V -> Src a -> Src T

{-
kind Cat = Term | Value
kind Form = General | Administrative Form

data L :: Cat ~> Form ~> *0 where
  Var :: Label l -> L Term General
  Lam :: Label l -> L a f -> L Value General
  App :: L a f -> L b g -> L Term General
  Let :: Label l -> L a f -> L b g -> L Term (Administrative f)
  LetRec :: [(Label l, L Value General)] -> L a f -> L Term (Administrative General)

anf :: L a f -> L Term (Administrative General)

-- Let reductions (from computational lambda calculus)
anf (App (Let x e1 e2) e3) = anf (Let x e1 (App e2 e3))
anf (App y (Let x e1 e2)) = anf (Let x e1 (App y e2))
anf (Let x2 (Let x1 e1 e2) e) = anf (Let x1 e1 (Let x2 e2 e))

-- LetRec reductions (from cyclic call-by-value calculus)
anf (App (LetRec d e) e') = anf (LetRec d (App e e'))
anf (App y (LetRec d e)) = anf (LetRec d (App y e))
anf (Let x1 (LetRec d e1) e) = LetRec d (Let x1 e1 e)

-- idempotent forms
anf (i@(Let _ (Var _) _)) = i
anf (i@(Let _ (Lam _ _) _)) = i
anf (i@(Let _ (App _ _) _)) = i
anf (i@(LetRec _ _)) = i

-- kill-all rule
anf (e@(Var _)) = Let `fresh e (Var `fresh)
anf (e@(App _ _)) = Let `fresh e (Var `fresh)
anf (e@(Lam _ _)) = Let `fresh e (Var `fresh)


-- Section 2.3 -- Introduce the ANF language
kind YesNo = Yes | No
--                    Named? Lambda?
kind ANFCat = ANFTerm YesNo YesNo

data ANF :: ANFCat ~> *0 where
  ANFVar :: Label l -> ANF (ANFTerm Yes No)
  ANFLet :: Label l -> ANF (ANFTerm Yes a) -> ANF (ANFTerm a b) -> ANF (ANFTerm No No)
  ANFLetRec :: [(Label l, ANF (ANFTerm a Yes))] -> ANF (ANFTerm a b) -> ANF (ANFTerm No No)
  ANFLam :: Label l -> ANF a -> ANF (ANFTerm Yes Yes)
  ANFApp :: ANF (ANFTerm Yes No) -> ANF (ANFTerm Yes No) -> ANF (ANFTerm Yes No)

-- convert normalized source to ANF

--cat2lambda :: Cat ~> YesNo
--{cat2lambda Term} = No
--{cat2lambda Value} = Yes

cat2lambda' :: Cat ~> ANFCat
{cat2lambda' Term} = ANFTerm Yes No
{cat2lambda' Value} = ANFTerm Yes Yes
 
conv :: L Term (Administrative General) -> ANF (ANFTerm No No)
--conv (Let l e1 e2) = ANFLet l (conv' e1) (conv'' e2)
conv (Let l e1 e2) = ANFLet l (check (conv' e1)) (ANFVar l) -- cheat


-- expression conversions
conv' :: L a General -> ANF {cat2lambda' a}
--conv' :: L a General -> ANF (ANFTerm Yes {cat2lambda a}) -- BUG?

conv' (Var l) = ANFVar l

-}